the_es:ES, e, e':E.
(e < e')
 ((((first(e'))) c ((e < pred(e'))  (e = pred(e'))))
  ((isrcv(e')) c ((e < sender(e'))  (e = sender(e'))))) 

latex

Definitions	x:A. B(x), P  Q, P  Q, A c B, P & Q, P  Q, t  T, P  Q, , Trans(T;x,y.E(x;y))
Lemmas	es-axioms, es-causl wf, not wf, assert wf, es-first wf, es-pred wf, es-E wf, es-isrcv wf, es-sender wf, event system wf, es-pred-locl